#include <UnitTest++.h>
#include "formule.hpp"
#include "sat.hpp"
#include "parser.hpp"
#include <iostream>
// Exemple de test des fonctions de passage arbre de syntaxe abstraite <-> string
/*TEST(lit_ecrit_formule) {
  formule f = lit_formule("p /\\ (q => r \\/ p)");
  string s = formule2string(f);
  formule f2 = lit_formule(s);
  string s2 = formule2string(f2);
  CHECK(s == s2);
  free_all(f);
  free_all(f2);
}*/
//test sur les clauses
/*TEST(test_clause){
    cls_t cl1 = {1,4,6,7};
    cls_t cl2 = {8,5,7,1,3,26,9};
    cout << cl1 << endl;
    cout << cl2 << endl;
    CHECK(cl1 != cl2);
    CHECK(cl2 != cl1);
    CHECK(cl1 == cl1);
    CHECK(cl2 == cl2);
    cl1= {1,4,6};
    cl2 = {6,1,4};
    CHECK(cl1==cl2);
    
}*/
//test cnf
/*TEST(test_cnf){
    cls_t cls1 = {7,6,1,4,1};
    cls_t cls2 = {8,6,4,5,4,8,9,3,1};
    cnf_t cnf1 = {cls1,cls2};
    cout << cnf1 <<endl;
    CHECK(est_dans(cls1,cnf1));
    CHECK(est_dans(cls2,cnf1));
    
    cls_t cls3 = {7,1,1,4,5};
    CHECK(!est_dans(cls3,cnf1));
    
    cnf_t cnf3 = {{1,2,3},{3,4,5}};
    cnf_t cnf2 = {{3,5,4},{2,3,1}};
    CHECK(cnf3==cnf2);
}*/
//test numerote
/*TEST(test_numerote){
    formule f1,f2;
    map<string,var_t> map1;
    
    f1 = lit_formule("a\\/b<=>b\\/a");
    numerote(f1,map1);
    CHECK(map1.size() == 2);
    
    f2 = lit_formule(("c\\/d<=>~e"));
    numerote(f2,map1);
    
    CHECK(map1.size() == 5);
    
    map<string,var_t> map2;
    f2 = lit_formule(("a\\/b=>c"));
    numerote(f2,map2);
cout << map2["a"] << endl;
cout << map2["b"] << endl;
cout << map2["c"] << endl;
    CHECK(map2.size() == 3);
    
}*/
/*TEST(test_varToLit){
    var_t t=5;
    CHECK(var2lit(t)==2);
    CHECK(var2lit(t,false)==3);
    
cout << var2lit(t) << endl;
    lit_t l = 2;
    CHECK(neg(l)==3);
    
    l=3;
    CHECK(neg(l)==2);
}*/
/*TEST(lit2var){
    lit_t l= 2;
    CHECK(lit2var(l)==1);
    
    l=3;
    CHECK(lit2var(l)==1);
    
    l=12;
    CHECK(lit2var(l)==6);
    
    l=13;
    CHECK(lit2var(l)==6);
}*/
/*TEST(test_positif){
    lit_t l=6;
    CHECK(positif(l));
    
    l=5;
    CHECK(!positif(l));
}*/
//test de transfo de tseitin
/*TEST(tseitin_a_ou_b_imp_c){
    cnf_t cnf_tseitin = tseitin(lit_formule("a\\/b=>c"));
    cnf_t cnf_attendue = {{7,0,2},{6,1},{6,3},{9,7,4},{8,6},{8,5},{8}};
    
cout <<  cnf_tseitin << endl;
cout <<  cnf_attendue;
    CHECK(cnf_tseitin == cnf_attendue);
}*/
/*TEST(valeure_cnf){
    //tests valeure_lit
    vector<val_t> vec = {FAUX};
    CHECK(valeur_lit(vec,0)==FAUX);
    CHECK(valeur_lit(vec,1)==VRAI);
    
    vec.push_back(INDETERMINEE);
    CHECK(valeur_lit(vec,2)==INDETERMINEE);
    CHECK(valeur_lit(vec,3)==INDETERMINEE);
    
    vec.push_back(VRAI);
    CHECK(valeur_lit(vec,4)==VRAI);
    CHECK(valeur_lit(vec,5)==FAUX);
    
    //tests valeure_clause
    cls_t cl1 = {0,2,4};
    CHECK(valeur_clause(vec,cl1)==VRAI);
    
    vec.push_back(INDETERMINEE);
    vec.push_back(INDETERMINEE);
    vec.push_back(VRAI);
    cls_t cl2 = {6,8,10};
    CHECK(valeur_clause(vec,cl2) == VRAI);
    
    vec.push_back(FAUX);
    vec.push_back(INDETERMINEE);
    cls_t cl3 = {12,14};
    CHECK(valeur_clause(vec,cl3)==INDETERMINEE);
    
    vec.push_back(FAUX);
    vec.push_back(FAUX);
    cls_t cl4 = {16,18};
    CHECK(valeur_clause(vec,cl4)==FAUX);
    
    //tests valeure cnf
    cnf_t cnf1 = {cl1,cl2};
    CHECK(valeur_cnf(vec,cnf1)==VRAI);
    
    cnf_t cnf2 = {cl1,cl2,cl3,cl4};
    CHECK(valeur_cnf(vec,cnf2)==FAUX);
    
    cnf_t cnf3 = {cl1,cl2,cl3};
    CHECK(valeur_cnf(vec,cnf3)==INDETERMINEE);
    
    
}*/
/*TEST(cherche){
    formule f = lit_formule("a");
    vector<val_t> vec = {INDETERMINEE};
    cnf_t cnf = tseitin(f);
    
    CHECK(cherche(vec,0,cnf));
    
    formule f2 = lit_formule("a/\\~a");
    cnf_t cnf2 = tseitin(f2);
    vector<val_t> vec2 = {INDETERMINEE,INDETERMINEE};
    CHECK(!cherche(vec2,0,cnf));
    
    }*/
/*TEST(applique)
{
    formule f = lit_formule("a => b");
    formule f2 = lit_formule("(p => q)");
    formule res;
     map<string,formule> substitution;
    substitution.insert(pair<string,formule>("a",lit_formule("p")));    
    substitution.insert(pair<string,formule>("b",lit_formule("q")));
    res = applique(f,substitution);
cout << f << endl;
cout << res;
    CHECK(f2 == res);
    
}*/
/*TEST(index_clauses)
{
    formule f = lit_formule("a => b");
    cnf_t cnf_tseitin = tseitin(f);

    cout << cnf_tseitin << endl;

    vector<vector<cls_t>> indexe = indexe_clauses(cnf_tseitin);

    for(unsigned int i = 0 ; i < indexe.size() ; i++)
    {
        for(unsigned int j = 0 ; j < indexe[i].size() ; j++)
        {
            cout  << "v["<< i << "]" << indexe[i][j] << "\n";            
        }
    }
}*/
int main()
{
  return UnitTest::RunAllTests(); // un peu magique: lance tous les tests
}
